$\forall$${\it es}$:ES, $C$:Type, ${\it out}$:($C$$\rightarrow$IdLnk), $d$:Id, $i$:$C$, $e$:E. fifo\_deliver(${\it es}$;${\it out}$;$d$;$i$;$e$) $\in$ $\mathbb{P}$